Left Termination proof of /tmp/tmpaI94jm/gopher1.pl

Left Termination of the query pattern
gopher(g,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog

↳1 PrologToPrologProblemTransformerProof (⇒, 81 ms)

↳2 Prolog

↳3 PrologToPiTRSProof (⇒, 16 ms)

↳4 PiTRS

↳5 DependencyPairsProof (⇔, 0 ms)

↳6 PiDP

↳7 DependencyGraphProof (⇔, 0 ms)

↳8 TRUE

(0) Obligation:

Clauses:

gopher(nil, L) :- ','(!, eq(L, nil)).
gopher(X, Y) :- ','(head(X, nil), ','(!, ','(tail(X, T), eq(Y, cons(nil, T))))).
gopher(X, Y) :- ','(head(X, H), ','(head(H, U), ','(tail(H, V), ','(tail(X, W), gopher(cons(U, cons(V, W)), Y))))).
head([], X1).
head(.(X, X2), X).
tail([], []).
tail(.(X3, X), X).
eq(X, X).

Query: gopher(g,a)

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph ICLP10.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: gopher(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: gopher(T1, T2), SCOPE: 1, CLAUSE: 0 | gopher(T1, T2), SCOPE: 1, CLAUSE: 1 | gopher(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: ','(!_1, eq(T5, nil)) | gopher(nil, T2), SCOPE: 1, CLAUSE: 1 | gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: gopher(T1, T2), SCOPE: 1, CLAUSE: 1 | gopher(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nX5 is free\ngopher(T1, T2) !=? gopher(nil, X5)", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: eq(T5, nil)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: eq(T5, nil), SCOPE: 2, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(head(T11, nil), ','(!_1, ','(tail(T11, X13), eq(T13, cons(nil, X13))))) | gopher(T11, T2), SCOPE: 1, CLAUSE: 2\n\nT11 is ground\nX5 is free\nX13 is free\ngopher(T11, T2) !=? gopher(nil, X5)", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(head(T11, nil), ','(!_1, ','(tail(T11, X13), eq(T13, cons(nil, X13))))), SCOPE: 3, CLAUSE: 3 | ','(head(T11, nil), ','(!_1, ','(tail(T11, X13), eq(T13, cons(nil, X13))))), SCOPE: 3, CLAUSE: 4 | ?_3 | gopher(T11, T2), SCOPE: 1, CLAUSE: 2\n\nT11 is ground\nX5 is free\nX13 is free\ngopher(T11, T2) !=? gopher(nil, X5)", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(!_1, ','(tail([], X13), eq(T13, cons(nil, X13)))) | ','(head([], nil), ','(!_1, ','(tail([], X13), eq(T13, cons(nil, X13))))), SCOPE: 3, CLAUSE: 4 | ?_3 | gopher([], T2), SCOPE: 1, CLAUSE: 2\n\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(head(T11, nil), ','(!_1, ','(tail(T11, X13), eq(T13, cons(nil, X13))))), SCOPE: 3, CLAUSE: 4 | ?_3 | gopher(T11, T2), SCOPE: 1, CLAUSE: 2\n\nT11 is ground\nX5 is free\nX13 is free\nX16 is free\ngopher(T11, T2) !=? gopher(nil, X5)\nhead(T11, nil) !=? head([], X16)", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(tail([], X13), eq(T13, cons(nil, X13)))\n\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(tail([], X13), eq(T13, cons(nil, X13))), SCOPE: 4, CLAUSE: 5 | ','(tail([], X13), eq(T13, cons(nil, X13))), SCOPE: 4, CLAUSE: 6\n\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(tail([], X13), eq(T13, cons(nil, X13))), SCOPE: 4, CLAUSE: 5\n\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(tail([], X13), eq(T13, cons(nil, X13))), SCOPE: 4, CLAUSE: 6\n\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: eq(T13, cons(nil, []))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: eq(T13, cons(nil, [])), SCOPE: 5, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(!_1, ','(tail(.(nil, T22), X13), eq(T13, cons(nil, X13)))) | ?_3 | gopher(.(nil, T22), T2), SCOPE: 1, CLAUSE: 2\n\nT22 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ?_3 | gopher(T11, T2), SCOPE: 1, CLAUSE: 2\n\nT11 is ground\nX5 is free\nX16 is free\nX26 is free\nX27 is free\ngopher(T11, T2) !=? gopher(nil, X5)\nhead(T11, nil) !=? head([], X16)\nhead(T11, nil) !=? head(.(X26, X27), X26)", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(tail(.(nil, T22), X13), eq(T13, cons(nil, X13)))\n\nT22 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ','(tail(.(nil, T22), X13), eq(T13, cons(nil, X13))), SCOPE: 6, CLAUSE: 5 | ','(tail(.(nil, T22), X13), eq(T13, cons(nil, X13))), SCOPE: 6, CLAUSE: 6\n\nT22 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(tail(.(nil, T22), X13), eq(T13, cons(nil, X13))), SCOPE: 6, CLAUSE: 6\n\nT22 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: eq(T13, cons(nil, T25))\n\nT25 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: eq(T13, cons(nil, T25)), SCOPE: 7, CLAUSE: 7\n\nT25 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: gopher(T11, T2), SCOPE: 1, CLAUSE: 2\n\nT11 is ground\nX5 is free\nX16 is free\nX26 is free\nX27 is free\ngopher(T11, T2) !=? gopher(nil, X5)\nhead(T11, nil) !=? head([], X16)\nhead(T11, nil) !=? head(.(X26, X27), X26)", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ','(head(T37, X48), ','(head(X48, X49), ','(tail(X48, X50), ','(tail(T37, X51), gopher(cons(X49, cons(X50, X51)), T39)))))\n\nT37 is ground\nX5 is free\nX16 is free\nX26 is free\nX27 is free\nX48 is free\nX49 is free\nX50 is free\nX51 is free\ngopher(T37, T2) !=? gopher(nil, X5)\nhead(T37, nil) !=? head([], X16)\nhead(T37, nil) !=? head(.(X26, X27), X26)", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(head(T37, X48), ','(head(X48, X49), ','(tail(X48, X50), ','(tail(T37, X51), gopher(cons(X49, cons(X50, X51)), T39))))), SCOPE: 8, CLAUSE: 3 | ','(head(T37, X48), ','(head(X48, X49), ','(tail(X48, X50), ','(tail(T37, X51), gopher(cons(X49, cons(X50, X51)), T39))))), SCOPE: 8, CLAUSE: 4\n\nT37 is ground\nX5 is free\nX16 is free\nX26 is free\nX27 is free\nX48 is free\nX49 is free\nX50 is free\nX51 is free\ngopher(T37, T2) !=? gopher(nil, X5)\nhead(T37, nil) !=? head([], X16)\nhead(T37, nil) !=? head(.(X26, X27), X26)", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(head(T37, X48), ','(head(X48, X49), ','(tail(X48, X50), ','(tail(T37, X51), gopher(cons(X49, cons(X50, X51)), T39))))), SCOPE: 8, CLAUSE: 4\n\nT37 is ground\nX5 is free\nX16 is free\nX26 is free\nX27 is free\nX48 is free\nX49 is free\nX50 is free\nX51 is free\ngopher(T37, T2) !=? gopher(nil, X5)\nhead(T37, nil) !=? head([], X16)\nhead(T37, nil) !=? head(.(X26, X27), X26)", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(head(T44, X49), ','(tail(T44, X50), ','(tail(.(T44, T45), X51), gopher(cons(X49, cons(X50, X51)), T39))))\n\nT44 is ground\nT45 is ground\nX26 is free\nX27 is free\nX49 is free\nX50 is free\nX51 is free\nhead(.(T44, T45), nil) !=? head(.(X26, X27), X26)", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(head(T44, X49), ','(tail(T44, X50), ','(tail(.(T44, T45), X51), gopher(cons(X49, cons(X50, X51)), T39)))), SCOPE: 9, CLAUSE: 3 | ','(head(T44, X49), ','(tail(T44, X50), ','(tail(.(T44, T45), X51), gopher(cons(X49, cons(X50, X51)), T39)))), SCOPE: 9, CLAUSE: 4\n\nT44 is ground\nT45 is ground\nX26 is free\nX27 is free\nX49 is free\nX50 is free\nX51 is free\nhead(.(T44, T45), nil) !=? head(.(X26, X27), X26)", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ','(head(T44, X49), ','(tail(T44, X50), ','(tail(.(T44, T45), X51), gopher(cons(X49, cons(X50, X51)), T39)))), SCOPE: 9, CLAUSE: 3\n\nT44 is ground\nT45 is ground\nX26 is free\nX27 is free\nX49 is free\nX50 is free\nX51 is free\nhead(.(T44, T45), nil) !=? head(.(X26, X27), X26)", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: ','(head(T44, X49), ','(tail(T44, X50), ','(tail(.(T44, T45), X51), gopher(cons(X49, cons(X50, X51)), T39)))), SCOPE: 9, CLAUSE: 4\n\nT44 is ground\nT45 is ground\nX26 is free\nX27 is free\nX49 is free\nX50 is free\nX51 is free\nhead(.(T44, T45), nil) !=? head(.(X26, X27), X26)", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(tail([], X50), ','(tail(.([], T45), X51), gopher(cons(X71, cons(X50, X51)), T39)))\n\nT45 is ground\nX50 is free\nX51 is free\nX71 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: ','(tail([], X50), ','(tail(.([], T45), X51), gopher(cons(X71, cons(X50, X51)), T39))), SCOPE: 10, CLAUSE: 5 | ','(tail([], X50), ','(tail(.([], T45), X51), gopher(cons(X71, cons(X50, X51)), T39))), SCOPE: 10, CLAUSE: 6\n\nT45 is ground\nX50 is free\nX51 is free\nX71 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(tail([], X50), ','(tail(.([], T45), X51), gopher(cons(X71, cons(X50, X51)), T39))), SCOPE: 10, CLAUSE: 5\n\nT45 is ground\nX50 is free\nX51 is free\nX71 is free", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: ','(tail([], X50), ','(tail(.([], T45), X51), gopher(cons(X71, cons(X50, X51)), T39))), SCOPE: 10, CLAUSE: 6\n\nT45 is ground\nX50 is free\nX51 is free\nX71 is free", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(tail(.([], T45), X51), gopher(cons(X71, cons([], X51)), T39))\n\nT45 is ground\nX51 is free\nX71 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(tail(.([], T45), X51), gopher(cons(X71, cons([], X51)), T39)), SCOPE: 11, CLAUSE: 5 | ','(tail(.([], T45), X51), gopher(cons(X71, cons([], X51)), T39)), SCOPE: 11, CLAUSE: 6\n\nT45 is ground\nX51 is free\nX71 is free", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(tail(.([], T45), X51), gopher(cons(X71, cons([], X51)), T39)), SCOPE: 11, CLAUSE: 6\n\nT45 is ground\nX51 is free\nX71 is free", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: gopher(cons(X71, cons([], T48)), T39)\n\nT48 is ground\nX71 is free", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: gopher(cons(X71, cons([], T48)), T39), SCOPE: 12, CLAUSE: 0 | gopher(cons(X71, cons([], T48)), T39), SCOPE: 12, CLAUSE: 1 | gopher(cons(X71, cons([], T48)), T39), SCOPE: 12, CLAUSE: 2\n\nT48 is ground\nX71 is free", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: gopher(cons(X71, cons([], T48)), T39), SCOPE: 12, CLAUSE: 1 | gopher(cons(X71, cons([], T48)), T39), SCOPE: 12, CLAUSE: 2\n\nT48 is ground\nX71 is free", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: ','(head(cons(X95, cons([], T54)), nil), ','(!_12, ','(tail(cons(X95, cons([], T54)), X94), eq(T56, cons(nil, X94))))) | gopher(cons(X71, cons([], T54)), T39), SCOPE: 12, CLAUSE: 2\n\nT54 is ground\nX71 is free\nX95 is free\nX94 is free", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(head(cons(X95, cons([], T54)), nil), ','(!_12, ','(tail(cons(X95, cons([], T54)), X94), eq(T56, cons(nil, X94))))), SCOPE: 13, CLAUSE: 3 | ','(head(cons(X95, cons([], T54)), nil), ','(!_12, ','(tail(cons(X95, cons([], T54)), X94), eq(T56, cons(nil, X94))))), SCOPE: 13, CLAUSE: 4 | ?_13 | gopher(cons(X71, cons([], T54)), T39), SCOPE: 12, CLAUSE: 2\n\nT54 is ground\nX71 is free\nX95 is free\nX94 is free", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ','(head(cons(X95, cons([], T54)), nil), ','(!_12, ','(tail(cons(X95, cons([], T54)), X94), eq(T56, cons(nil, X94))))), SCOPE: 13, CLAUSE: 4 | ?_13 | gopher(cons(X71, cons([], T54)), T39), SCOPE: 12, CLAUSE: 2\n\nT54 is ground\nX71 is free\nX95 is free\nX94 is free", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ?_13 | gopher(cons(X71, cons([], T54)), T39), SCOPE: 12, CLAUSE: 2\n\nT54 is ground\nX71 is free", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: gopher(cons(X71, cons([], T54)), T39), SCOPE: 12, CLAUSE: 2\n\nT54 is ground\nX71 is free", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(head(cons(X116, cons([], T62)), X112), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(cons(X116, cons([], T62)), X115), gopher(cons(X113, cons(X114, X115)), T64)))))\n\nT62 is ground\nX116 is free\nX112 is free\nX113 is free\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(head(cons(X116, cons([], T62)), X112), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(cons(X116, cons([], T62)), X115), gopher(cons(X113, cons(X114, X115)), T64))))), SCOPE: 14, CLAUSE: 3 | ','(head(cons(X116, cons([], T62)), X112), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(cons(X116, cons([], T62)), X115), gopher(cons(X113, cons(X114, X115)), T64))))), SCOPE: 14, CLAUSE: 4\n\nT62 is ground\nX116 is free\nX112 is free\nX113 is free\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ','(head(cons(X116, cons([], T62)), X112), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(cons(X116, cons([], T62)), X115), gopher(cons(X113, cons(X114, X115)), T64))))), SCOPE: 14, CLAUSE: 4\n\nT62 is ground\nX116 is free\nX112 is free\nX113 is free\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ','(tail(.(T69, T70), X50), ','(tail(.(.(T69, T70), T45), X51), gopher(cons(T69, cons(X50, X51)), T39)))\n\nT45 is ground\nT69 is ground\nT70 is ground\nX50 is free\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ','(tail(.(T69, T70), X50), ','(tail(.(.(T69, T70), T45), X51), gopher(cons(T69, cons(X50, X51)), T39))), SCOPE: 15, CLAUSE: 5 | ','(tail(.(T69, T70), X50), ','(tail(.(.(T69, T70), T45), X51), gopher(cons(T69, cons(X50, X51)), T39))), SCOPE: 15, CLAUSE: 6\n\nT45 is ground\nT69 is ground\nT70 is ground\nX50 is free\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: ','(tail(.(T69, T70), X50), ','(tail(.(.(T69, T70), T45), X51), gopher(cons(T69, cons(X50, X51)), T39))), SCOPE: 15, CLAUSE: 6\n\nT45 is ground\nT69 is ground\nT70 is ground\nX50 is free\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ','(tail(.(.(T75, T76), T45), X51), gopher(cons(T75, cons(T76, X51)), T39))\n\nT45 is ground\nT75 is ground\nT76 is ground\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: ','(tail(.(.(T75, T76), T45), X51), gopher(cons(T75, cons(T76, X51)), T39)), SCOPE: 16, CLAUSE: 5 | ','(tail(.(.(T75, T76), T45), X51), gopher(cons(T75, cons(T76, X51)), T39)), SCOPE: 16, CLAUSE: 6\n\nT45 is ground\nT75 is ground\nT76 is ground\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: ','(tail(.(.(T75, T76), T45), X51), gopher(cons(T75, cons(T76, X51)), T39)), SCOPE: 16, CLAUSE: 6\n\nT45 is ground\nT75 is ground\nT76 is ground\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: gopher(cons(T83, cons(T84, T85)), T39)\n\nT83 is ground\nT84 is ground\nT85 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 72 [arrowhead = none ];
72 -> 2;

73 [label="EVAL with clause\ngopher(nil, X5) :- ','(!_1, eq(X5, nil)).\nand substitutionT1 -> nil,\nT2 -> T5,\nX5 -> T5,\nT4 -> T5", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 73 [arrowhead = none ];
73 -> 3;

74 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
2 -> 74 [arrowhead = none ];
74 -> 4;

75 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 75 [arrowhead = none ];
75 -> 5;

76 [label="ONLY EVAL with clause\ngopher(X11, X12) :- ','(head(X11, nil), ','(!_1, ','(tail(X11, X13), eq(X12, cons(nil, X13))))).\nand substitutionT1 -> T11,\nX11 -> T11,\nT2 -> T13,\nX12 -> T13,\nT12 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 76 [arrowhead = none ];
76 -> 10;

77 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
5 -> 77 [arrowhead = none ];
77 -> 6;

78 [label="EVAL with clause\neq(X8, X8).\nand substitutionT5 -> nil,\nX8 -> nil,\nT8 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 78 [arrowhead = none ];
78 -> 7;

79 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
6 -> 79 [arrowhead = none ];
79 -> 8;

80 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
7 -> 80 [arrowhead = none ];
80 -> 9;

81 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
10 -> 81 [arrowhead = none ];
81 -> 11;

82 [label="EVAL with clause\nhead([], X16).\nand substitutionT11 -> [],\nX16 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 82 [arrowhead = none ];
82 -> 12;

83 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
11 -> 83 [arrowhead = none ];
83 -> 13;

84 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
12 -> 84 [arrowhead = none ];
84 -> 14;

85 [label="EVAL with clause\nhead(.(X26, X27), X26).\nand substitutionX26 -> nil,\nX27 -> T22,\nT11 -> .(nil, T22),\nT21 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 85 [arrowhead = none ];
85 -> 24;

86 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
13 -> 86 [arrowhead = none ];
86 -> 25;

87 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
14 -> 87 [arrowhead = none ];
87 -> 15;

88 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
15 -> 88 [arrowhead = none ];
88 -> 16;

89 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
15 -> 89 [arrowhead = none ];
89 -> 17;

90 [label="ONLY EVAL with clause\ntail([], []).\nand substitutionX13 -> []", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 90 [arrowhead = none ];
90 -> 18;

91 [label="BACKTRACK\nfor clause: tail(.(X3, X), X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 91 [arrowhead = none ];
91 -> 23;

92 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
18 -> 92 [arrowhead = none ];
92 -> 19;

93 [label="EVAL with clause\neq(X19, X19).\nand substitutionT13 -> cons(nil, []),\nX19 -> cons(nil, []),\nT16 -> cons(nil, [])", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 93 [arrowhead = none ];
93 -> 20;

94 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
19 -> 94 [arrowhead = none ];
94 -> 21;

95 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
20 -> 95 [arrowhead = none ];
95 -> 22;

96 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
24 -> 96 [arrowhead = none ];
96 -> 26;

97 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 97 [arrowhead = none ];
97 -> 34;

98 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
26 -> 98 [arrowhead = none ];
98 -> 27;

99 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 99 [arrowhead = none ];
99 -> 28;

100 [label="ONLY EVAL with clause\ntail(.(X32, X33), X33).\nand substitutionX32 -> nil,\nT22 -> T25,\nX33 -> T25,\nX13 -> T25", fontsize=14, style = filled, fillcolor = lightblue];
28 -> 100 [arrowhead = none ];
100 -> 29;

101 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
29 -> 101 [arrowhead = none ];
101 -> 30;

102 [label="EVAL with clause\neq(X36, X36).\nand substitutionT13 -> cons(nil, T31),\nX36 -> cons(nil, T31),\nT25 -> T31,\nT30 -> cons(nil, T31)", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 102 [arrowhead = none ];
102 -> 31;

103 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
30 -> 103 [arrowhead = none ];
103 -> 32;

104 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 104 [arrowhead = none ];
104 -> 33;

105 [label="ONLY EVAL with clause\ngopher(X46, X47) :- ','(head(X46, X48), ','(head(X48, X49), ','(tail(X48, X50), ','(tail(X46, X51), gopher(cons(X49, cons(X50, X51)), X47))))).\nand substitutionT11 -> T37,\nX46 -> T37,\nT2 -> T39,\nX47 -> T39,\nT38 -> T39", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 105 [arrowhead = none ];
105 -> 35;

106 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
35 -> 106 [arrowhead = none ];
106 -> 36;

107 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (head(T37, nil), head([], X16))", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 107 [arrowhead = none ];
107 -> 37;

108 [label="EVAL with clause\nhead(.(X59, X60), X59).\nand substitutionX59 -> T44,\nX60 -> T45,\nT37 -> .(T44, T45),\nX48 -> T44", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 108 [arrowhead = none ];
108 -> 38;

109 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
37 -> 109 [arrowhead = none ];
109 -> 39;

110 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
38 -> 110 [arrowhead = none ];
110 -> 40;

111 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
40 -> 111 [arrowhead = none ];
111 -> 41;

112 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
40 -> 112 [arrowhead = none ];
112 -> 42;

113 [label="EVAL with clause\nhead([], X70).\nand substitutionT44 -> [],\nX49 -> X71,\nX70 -> X71", fontsize=14, style = filled, fillcolor = lightblue];
41 -> 113 [arrowhead = none ];
113 -> 43;

114 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
41 -> 114 [arrowhead = none ];
114 -> 44;

115 [label="EVAL with clause\nhead(.(X127, X128), X127).\nand substitutionX127 -> T69,\nX128 -> T70,\nT44 -> .(T69, T70),\nX49 -> T69", fontsize=14, style = filled, fillcolor = lightblue];
42 -> 115 [arrowhead = none ];
115 -> 64;

116 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
42 -> 116 [arrowhead = none ];
116 -> 65;

117 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
43 -> 117 [arrowhead = none ];
117 -> 45;

118 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
45 -> 118 [arrowhead = none ];
118 -> 46;

119 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
45 -> 119 [arrowhead = none ];
119 -> 47;

120 [label="ONLY EVAL with clause\ntail([], []).\nand substitutionX50 -> []", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 120 [arrowhead = none ];
120 -> 48;

121 [label="BACKTRACK\nfor clause: tail(.(X3, X), X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
47 -> 121 [arrowhead = none ];
121 -> 63;

122 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
48 -> 122 [arrowhead = none ];
122 -> 49;

123 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 123 [arrowhead = none ];
123 -> 50;

124 [label="ONLY EVAL with clause\ntail(.(X81, X82), X82).\nand substitutionX81 -> [],\nT45 -> T48,\nX82 -> T48,\nX51 -> T48", fontsize=14, style = filled, fillcolor = lightblue];
50 -> 124 [arrowhead = none ];
124 -> 51;

125 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
51 -> 125 [arrowhead = none ];
125 -> 52;

126 [label="BACKTRACK\nfor clause: gopher(nil, L) :- ','(!, eq(L, nil))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
52 -> 126 [arrowhead = none ];
126 -> 53;

127 [label="ONLY EVAL with clause\ngopher(X92, X93) :- ','(head(X92, nil), ','(!_12, ','(tail(X92, X94), eq(X93, cons(nil, X94))))).\nand substitutionX71 -> X95,\nT48 -> T54,\nX92 -> cons(X95, cons([], T54)),\nT39 -> T56,\nX93 -> T56,\nT55 -> T56", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 127 [arrowhead = none ];
127 -> 54;

128 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
54 -> 128 [arrowhead = none ];
128 -> 55;

129 [label="BACKTRACK\nfor clause: head([], X1)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
55 -> 129 [arrowhead = none ];
129 -> 56;

130 [label="BACKTRACK\nfor clause: head(.(X, X2), X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
56 -> 130 [arrowhead = none ];
130 -> 57;

131 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
57 -> 131 [arrowhead = none ];
131 -> 58;

132 [label="ONLY EVAL with clause\ngopher(X110, X111) :- ','(head(X110, X112), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(X110, X115), gopher(cons(X113, cons(X114, X115)), X111))))).\nand substitutionX71 -> X116,\nT54 -> T62,\nX110 -> cons(X116, cons([], T62)),\nT39 -> T64,\nX111 -> T64,\nT63 -> T64", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 132 [arrowhead = none ];
132 -> 59;

133 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
59 -> 133 [arrowhead = none ];
133 -> 60;

134 [label="BACKTRACK\nfor clause: head([], X1)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
60 -> 134 [arrowhead = none ];
134 -> 61;

135 [label="BACKTRACK\nfor clause: head(.(X, X2), X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
61 -> 135 [arrowhead = none ];
135 -> 62;

136 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
64 -> 136 [arrowhead = none ];
136 -> 66;

137 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
66 -> 137 [arrowhead = none ];
137 -> 67;

138 [label="ONLY EVAL with clause\ntail(.(X135, X136), X136).\nand substitutionT69 -> T75,\nX135 -> T75,\nT70 -> T76,\nX136 -> T76,\nX50 -> T76", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 138 [arrowhead = none ];
138 -> 68;

139 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
68 -> 139 [arrowhead = none ];
139 -> 69;

140 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
69 -> 140 [arrowhead = none ];
140 -> 70;

141 [label="ONLY EVAL with clause\ntail(.(X143, X144), X144).\nand substitutionT75 -> T83,\nT76 -> T84,\nX143 -> .(T83, T84),\nT45 -> T85,\nX144 -> T85,\nX51 -> T85", fontsize=14, style = filled, fillcolor = lightblue];
70 -> 141 [arrowhead = none ];
141 -> 71;

142 [label="INSTANCE with matching:\nT1 -> cons(T83, cons(T84, T85))\nT2 -> T39", fontsize=14, style = filled, fillcolor = lightgrey];
71 -> 142 [arrowhead = none , style=dashed];
142 -> 1[style=dashed];

}

(2) Obligation:

Clauses:

gopherA(nil, nil).
gopherA([], cons(nil, [])).
gopherA(.(nil, T31), cons(nil, T31)).
gopherA(.(.(T83, T84), T85), T39) :- gopherA(cons(T83, cons(T84, T85)), T39).

Query: gopherA(g,a)

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
gopherA_in: (b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

gopherA_in_ga(nil, nil) → gopherA_out_ga(nil, nil)
gopherA_in_ga([], cons(nil, [])) → gopherA_out_ga([], cons(nil, []))
gopherA_in_ga(.(nil, T31), cons(nil, T31)) → gopherA_out_ga(.(nil, T31), cons(nil, T31))
gopherA_in_ga(.(.(T83, T84), T85), T39) → U1_ga(T83, T84, T85, T39, gopherA_in_ga(cons(T83, cons(T84, T85)), T39))
U1_ga(T83, T84, T85, T39, gopherA_out_ga(cons(T83, cons(T84, T85)), T39)) → gopherA_out_ga(.(.(T83, T84), T85), T39)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

gopherA_in_ga(nil, nil) → gopherA_out_ga(nil, nil)
gopherA_in_ga([], cons(nil, [])) → gopherA_out_ga([], cons(nil, []))
gopherA_in_ga(.(nil, T31), cons(nil, T31)) → gopherA_out_ga(.(nil, T31), cons(nil, T31))
gopherA_in_ga(.(.(T83, T84), T85), T39) → U1_ga(T83, T84, T85, T39, gopherA_in_ga(cons(T83, cons(T84, T85)), T39))
U1_ga(T83, T84, T85, T39, gopherA_out_ga(cons(T83, cons(T84, T85)), T39)) → gopherA_out_ga(.(.(T83, T84), T85), T39)

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

GOPHERA_IN_GA(.(.(T83, T84), T85), T39) → U1_GA(T83, T84, T85, T39, gopherA_in_ga(cons(T83, cons(T84, T85)), T39))
GOPHERA_IN_GA(.(.(T83, T84), T85), T39) → GOPHERA_IN_GA(cons(T83, cons(T84, T85)), T39)

The TRS R consists of the following rules:

gopherA_in_ga(nil, nil) → gopherA_out_ga(nil, nil)
gopherA_in_ga([], cons(nil, [])) → gopherA_out_ga([], cons(nil, []))
gopherA_in_ga(.(nil, T31), cons(nil, T31)) → gopherA_out_ga(.(nil, T31), cons(nil, T31))
gopherA_in_ga(.(.(T83, T84), T85), T39) → U1_ga(T83, T84, T85, T39, gopherA_in_ga(cons(T83, cons(T84, T85)), T39))
U1_ga(T83, T84, T85, T39, gopherA_out_ga(cons(T83, cons(T84, T85)), T39)) → gopherA_out_ga(.(.(T83, T84), T85), T39)

The argument filtering Pi contains the following mapping:
gopherA_in_ga(x1, x2) = gopherA_in_ga(x1)
nil = nil
gopherA_out_ga(x1, x2) = gopherA_out_ga(x2)
[] = []
.(x1, x2) = .(x1, x2)
U1_ga(x1, x2, x3, x4, x5) = U1_ga(x5)
cons(x1, x2) = cons(x1, x2)
GOPHERA_IN_GA(x1, x2) = GOPHERA_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5) = U1_GA(x5)

We have to consider all (P,R,Pi)-chains

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

GOPHERA_IN_GA(.(.(T83, T84), T85), T39) → U1_GA(T83, T84, T85, T39, gopherA_in_ga(cons(T83, cons(T84, T85)), T39))
GOPHERA_IN_GA(.(.(T83, T84), T85), T39) → GOPHERA_IN_GA(cons(T83, cons(T84, T85)), T39)

The TRS R consists of the following rules:

gopherA_in_ga(nil, nil) → gopherA_out_ga(nil, nil)
gopherA_in_ga([], cons(nil, [])) → gopherA_out_ga([], cons(nil, []))
gopherA_in_ga(.(nil, T31), cons(nil, T31)) → gopherA_out_ga(.(nil, T31), cons(nil, T31))
gopherA_in_ga(.(.(T83, T84), T85), T39) → U1_ga(T83, T84, T85, T39, gopherA_in_ga(cons(T83, cons(T84, T85)), T39))
U1_ga(T83, T84, T85, T39, gopherA_out_ga(cons(T83, cons(T84, T85)), T39)) → gopherA_out_ga(.(.(T83, T84), T85), T39)

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 0 SCCs with 2 less nodes.

(0) Obligation:

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) PrologToPiTRSProof (SOUND transformation)

(4) Obligation:

(5) DependencyPairsProof (EQUIVALENT transformation)

(6) Obligation:

(7) DependencyGraphProof (EQUIVALENT transformation)

(8) TRUE